Definitions | x << y, #$n, ||as||, (x l), Atom$n, no_repeats(T;l), adjacent(T;L;x;y), L1 L2, hd(l), a < b, P Q, e c e', {x:A| B(x)} , e  X, E, P & Q,  x. t(x), x.A(x), pred(e), <a, b>, first(e), suptype(S; T), S T, Top, x:A.B(x),  x,y. t(x;y), pred!(e;e'), SWellFounded(R(x;y)), constant_function(f;A;B), b, , e < e', r s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , type List, Msg(M), kind(e), loc(e), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), EOrderAxioms(E; pred?; info), IdLnk, left + right, Unit, EqDecider(T), , a:A fp B(a), EState(T), A, !Void(), P  Q, strong-subtype(A;B), False, chain-consistent(f;chain), sys-antecedent(es;Sys), AbsInterface(A), Type, ES, x:A. B(x), E(X), , x:A B(x), x before y l, Id, x:A. B(x), x:A B(x), s = t, f(a), t T, , {T}, increasing(f;k) |